IUnivRecord.agda:3,8-11
The sort of Bad cannot be the interval universe IUniv
when checking the definition of Bad
